(set-logic QF_UFBV)
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun x1 () (_ BitVec 1))
(declare-fun x2 () (_ BitVec 1))
(declare-const v4 Bool)
(declare-const v23 Bool)
(declare-const v1 Bool)
(assert (= v23 (xor true (xor true v1 v1 (bvule x1 (_ bv0 1)) true true false false v1) true (or (not v4) b1) true) (= ((_ extract 3 3) (bvnand (_ bv0 7) (_ bv0 7))) x2 ((_ extract 3 3) (bvnand (_ bv0 7) (_ bv0 7))) ((_ extract 3 3) (bvnand (_ bv0 7) (_ bv0 7))))))
(assert b2)
(check-sat)
